Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

INVARIANT TEST #83

Open
wants to merge 171 commits into
base: temp-invariant
Choose a base branch
from
Open

INVARIANT TEST #83

wants to merge 171 commits into from

Conversation

GalloDaSballo
Copy link
Collaborator

This is just a way for our tool to detected pushes to main and paste the result of the Invariant Testing Run

danielattilasimon and others added 30 commits November 19, 2024 10:11
As value now encodes timestamp, it would never be zero, we need to
decode and then check.
Both LUSD and LQTY are already safe.
Needed for `vm.expectPartialRevert()`
The fetched state doesn't change much depending on fuzz inputs,
so having a different seed each time won't result in drastically
increased RPC usage.

That is, once we fix the tests, because the Foundry action only
saves the RPC cache if the tests are passing. (Why though)?
It was taking 20 minutes for a single test run.
fix: Remove safeTransfer from UserProxy
fix: Remove ForwardBribe contract
If you pass any amount higher than your stake, and LQTYStaking will
internally truncate it to the maximum withdrawable amount.
Copy link

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

  • Fuzzer: ECHIDNA
  • Duration: 2h35m17s
  • Coverage: 43798
  • Failed: 7
  • Passed: 81

Results

Property Status
initiative_claimBribes(uint256,uint256,uint256,uint8)
check_unregisterable_consistecy(uint8)
check_claimable_solvency()
excludeSenders()
property_shouldNeverRevertgetInitiativeState(uint8)
check_realized_claiming_solvency()
targetInterfaces()
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)
helper_accrueBold(uint256)
property_BI02()
property_computingGlobalPowerNeverReverts()
governance_resetAllocations()
property_initiative_offset_matches_user_when_non_zero()
targetSenders()
targetContracts()
property_shouldGetTotalVotesAndState()
property_BI10()
property_shouldNeverRevertcalculateVotingThreshold()
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)
property_sum_of_user_voting_weights_strict()
property_sum_of_user_initiative_allocations()
property_summingInitiativesPowerNeverReverts()
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)
property_user_offset_is_always_greater_than_start()
helper_deployInitiative()
property_sum_of_lqty_global_user_matches()
property_sum_of_votes_in_bribes_match()
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)
targetArtifactSelectors()
property_sum_of_lqty_initiative_user_matches()
property_GV01()
property_viewCalculateVotingThreshold()
governance_registerInitiative(uint8)
initiative_depositBribe(uint256,uint256,uint256,uint8)
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)
property_BI07()
governance_resetAllocations_user_2()
targetArtifacts()
withdrwaMustFailOnNonZeroAcc(uint256)
property_sum_of_initatives_matches_total_votes_bounded()
property_BI04()
targetSelectors()
property_resetting_never_reverts(address[])
governance_depositLQTY_2(uint256)
governance_depositLQTY(uint256)
check_warmup_unregisterable_consistency(uint8)
property_ensure_user_alloc_cannot_dos()
property_BI08()
governance_withdrawLQTY(uint256)
property_sum_of_initatives_matches_total_votes_insolvency_assertion()
property_shouldNeverRevertgetLatestVotingThreshold()
governance_claimForInitiativeDoesntRevert(uint8)
property_BI03()
excludeSelectors()
excludeArtifacts()
check_claim_soundness()
property_shouldNeverRevertsecondsWithinEpoch()
failed()
property_sum_of_user_voting_weights_bounded()
property_BI01()
property_shouldNeverRevertepochStart(uint8)
property_BI09()
property_shouldNeverRevertSnapshotAndState(uint8)
property_shouldNeverRevertlqtyToVotes()
governance_snapshotVotesForInitiative(address)
governance_deployUserProxy()
depositMustFailOnNonZeroAlloc(uint256)
offsetIsRational(uint256)
property_allocations_are_never_dangerously_high()
property_global_offset_is_always_greater_than_start()
property_shouldNeverRevertgetTotalVotesAndState()
clamped_claimBribes(uint8)
property_shouldNeverRevertepoch()
governance_claimForInitiative(uint8)
property_GV_09()
excludeContracts()
governance_claimForInitiativeFuzzTest(uint8)
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)
property_viewTotalVotesAndStateEquivalency()
check_skip_consistecy(uint8)
governance_unregisterInitiative(uint8)
governance_claimFromStakingV1(uint8)
governance_allocateLQTY(int256[],int256[])
IS_TEST()
governance_depositLQTYViaPermit(uint256)
property_shouldNeverRevertgetInitiativeState_arbitrary(address)
property_sum_of_initatives_matches_total_votes_strict()
AssertionFailed(..)

Broken Properties

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

// forge test --match-test test_governance_withdrawLQTY_shouldRevertWhenClamped_ -vv 
 function test_governance_withdrawLQTY_shouldRevertWhenClamped_() public {

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_user_offset_is_always_greater_than_start_ -vv 
 function test_property_user_offset_is_always_greater_than_start_() public {

    vm.warp(block.timestamp + 605005);

    vm.roll(block.number + 1);

    governance_depositLQTY_2(2);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

// forge test --match-test test_property_sum_of_lqty_initiative_user_matches_ -vv 
 function test_property_sum_of_lqty_initiative_user_matches_() public {

    vm.warp(block.timestamp + 604956);

    vm.roll(block.number + 1);

    governance_depositLQTY_2(2);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

// forge test --match-test test_withdrwaMustFailOnNonZeroAcc_ -vv 
 function test_withdrwaMustFailOnNonZeroAcc_() public {

    offsetIsRational(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

// forge test --match-test test_property_resetting_never_reverts_ -vv 
 function test_property_resetting_never_reverts_() public {

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

// forge test --match-test test_depositMustFailOnNonZeroAlloc_ -vv 
 function test_depositMustFailOnNonZeroAlloc_() public {

    offsetIsRational(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_global_offset_is_always_greater_than_start_ -vv 
 function test_property_global_offset_is_always_greater_than_start_() public {

    vm.warp(block.timestamp + 561860);

    vm.roll(block.number + 1);

    governance_depositLQTY_2(2);

    vm.warp(block.timestamp + 42946);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

Copy link

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

  • Fuzzer: ECHIDNA
  • Duration: 2h30m38s
  • Coverage: 43449
  • Failed: 8
  • Passed: 80

Results

Property Status
initiative_claimBribes(uint256,uint256,uint256,uint8)
check_unregisterable_consistecy(uint8)
check_claimable_solvency()
excludeSenders()
property_shouldNeverRevertgetInitiativeState(uint8)
check_realized_claiming_solvency()
targetInterfaces()
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)
helper_accrueBold(uint256)
property_BI02()
property_computingGlobalPowerNeverReverts()
governance_resetAllocations()
property_initiative_offset_matches_user_when_non_zero()
targetSenders()
targetContracts()
property_shouldGetTotalVotesAndState()
property_BI10()
property_shouldNeverRevertcalculateVotingThreshold()
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)
property_sum_of_user_voting_weights_strict()
property_sum_of_user_initiative_allocations()
property_summingInitiativesPowerNeverReverts()
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)
property_user_offset_is_always_greater_than_start()
helper_deployInitiative()
property_sum_of_lqty_global_user_matches()
property_sum_of_votes_in_bribes_match()
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)
targetArtifactSelectors()
property_sum_of_lqty_initiative_user_matches()
property_GV01()
property_viewCalculateVotingThreshold()
governance_registerInitiative(uint8)
initiative_depositBribe(uint256,uint256,uint256,uint8)
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)
property_BI07()
governance_resetAllocations_user_2()
targetArtifacts()
withdrwaMustFailOnNonZeroAcc(uint256)
property_sum_of_initatives_matches_total_votes_bounded()
property_BI04()
targetSelectors()
property_resetting_never_reverts(address[])
governance_depositLQTY_2(uint256)
governance_depositLQTY(uint256)
check_warmup_unregisterable_consistency(uint8)
property_ensure_user_alloc_cannot_dos()
property_BI08()
governance_withdrawLQTY(uint256)
property_sum_of_initatives_matches_total_votes_insolvency_assertion()
property_shouldNeverRevertgetLatestVotingThreshold()
governance_claimForInitiativeDoesntRevert(uint8)
property_BI03()
excludeSelectors()
excludeArtifacts()
check_claim_soundness()
property_shouldNeverRevertsecondsWithinEpoch()
failed()
property_sum_of_user_voting_weights_bounded()
property_BI01()
property_shouldNeverRevertepochStart(uint8)
property_BI09()
property_shouldNeverRevertSnapshotAndState(uint8)
property_shouldNeverRevertlqtyToVotes()
governance_snapshotVotesForInitiative(address)
governance_deployUserProxy()
depositMustFailOnNonZeroAlloc(uint256)
offsetIsRational(uint256)
property_allocations_are_never_dangerously_high()
property_global_offset_is_always_greater_than_start()
property_shouldNeverRevertgetTotalVotesAndState()
clamped_claimBribes(uint8)
property_shouldNeverRevertepoch()
governance_claimForInitiative(uint8)
property_GV_09()
excludeContracts()
governance_claimForInitiativeFuzzTest(uint8)
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)
property_viewTotalVotesAndStateEquivalency()
check_skip_consistecy(uint8)
governance_unregisterInitiative(uint8)
governance_claimFromStakingV1(uint8)
governance_allocateLQTY(int256[],int256[])
IS_TEST()
governance_depositLQTYViaPermit(uint256)
property_shouldNeverRevertgetInitiativeState_arbitrary(address)
property_sum_of_initatives_matches_total_votes_strict()
AssertionFailed(..)

Broken Properties

Broken property:

check_unregisterable_consistecy

Sequence

// forge test --match-test test_check_unregisterable_consistecy_ -vv 
 function test_check_unregisterable_consistecy_() public {

    governance_depositLQTY_2(2);

    vm.warp(block.timestamp + 967925);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,0,1);

    vm.warp(block.timestamp + 241697);

    vm.roll(block.number + 1);

    governance_resetAllocations_user_2();

    check_unregisterable_consistecy(0);

 }

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

// forge test --match-test test_governance_withdrawLQTY_shouldRevertWhenClamped_ -vv 
 function test_governance_withdrawLQTY_shouldRevertWhenClamped_() public {

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_user_offset_is_always_greater_than_start_ -vv 
 function test_property_user_offset_is_always_greater_than_start_() public {

    governance_depositLQTY(1);

    vm.warp(block.timestamp + 168835);

    vm.roll(block.number + 1);

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 436212);
    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

// forge test --match-test test_property_sum_of_lqty_initiative_user_matches_ -vv 
 function test_property_sum_of_lqty_initiative_user_matches_() public {

    governance_depositLQTY_2(2);

    vm.warp(block.timestamp + 498929);

    vm.roll(block.number + 1);

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 105932);
    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

// forge test --match-test test_withdrwaMustFailOnNonZeroAcc_ -vv 
 function test_withdrwaMustFailOnNonZeroAcc_() public {

    offsetIsRational(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

// forge test --match-test test_property_resetting_never_reverts_ -vv 
 function test_property_resetting_never_reverts_() public {

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

// forge test --match-test test_depositMustFailOnNonZeroAlloc_ -vv 
 function test_depositMustFailOnNonZeroAlloc_() public {

    offsetIsRational(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_global_offset_is_always_greater_than_start_ -vv 
 function test_property_global_offset_is_always_greater_than_start_() public {

    vm.warp(block.timestamp + 314397);

    vm.roll(block.number + 1);

    governance_depositLQTY(1);

    vm.warp(block.timestamp + 290694);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

refactor: expose constant that can be returned by public getter
Copy link

Recon Campaign Started

feat: don't call `onAfterAllocateLQTY()` on vetos
Copy link

Recon Campaign Started

Copy link

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

  • Fuzzer: ECHIDNA
  • Duration: 2h27m44s
  • Coverage: 43510
  • Failed: 7
  • Passed: 81

Results

Property Status
initiative_claimBribes(uint256,uint256,uint256,uint8)
check_unregisterable_consistecy(uint8)
check_claimable_solvency()
excludeSenders()
property_shouldNeverRevertgetInitiativeState(uint8)
check_realized_claiming_solvency()
targetInterfaces()
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)
helper_accrueBold(uint256)
property_BI02()
property_computingGlobalPowerNeverReverts()
governance_resetAllocations()
property_initiative_offset_matches_user_when_non_zero()
targetSenders()
targetContracts()
property_shouldGetTotalVotesAndState()
property_BI10()
property_shouldNeverRevertcalculateVotingThreshold()
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)
property_sum_of_user_voting_weights_strict()
property_sum_of_user_initiative_allocations()
property_summingInitiativesPowerNeverReverts()
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)
property_user_offset_is_always_greater_than_start()
helper_deployInitiative()
property_sum_of_lqty_global_user_matches()
property_sum_of_votes_in_bribes_match()
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)
targetArtifactSelectors()
property_sum_of_lqty_initiative_user_matches()
property_GV01()
property_viewCalculateVotingThreshold()
governance_registerInitiative(uint8)
initiative_depositBribe(uint256,uint256,uint256,uint8)
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)
property_BI07()
governance_resetAllocations_user_2()
targetArtifacts()
withdrwaMustFailOnNonZeroAcc(uint256)
property_sum_of_initatives_matches_total_votes_bounded()
property_BI04()
targetSelectors()
property_resetting_never_reverts(address[])
governance_depositLQTY_2(uint256)
governance_depositLQTY(uint256)
check_warmup_unregisterable_consistency(uint8)
property_ensure_user_alloc_cannot_dos()
property_BI08()
governance_withdrawLQTY(uint256)
property_sum_of_initatives_matches_total_votes_insolvency_assertion()
property_shouldNeverRevertgetLatestVotingThreshold()
governance_claimForInitiativeDoesntRevert(uint8)
property_BI03()
excludeSelectors()
excludeArtifacts()
check_claim_soundness()
property_shouldNeverRevertsecondsWithinEpoch()
failed()
property_sum_of_user_voting_weights_bounded()
property_BI01()
property_shouldNeverRevertepochStart(uint8)
property_BI09()
property_shouldNeverRevertSnapshotAndState(uint8)
property_shouldNeverRevertlqtyToVotes()
governance_snapshotVotesForInitiative(address)
governance_deployUserProxy()
depositMustFailOnNonZeroAlloc(uint256)
offsetIsRational(uint256)
property_allocations_are_never_dangerously_high()
property_global_offset_is_always_greater_than_start()
property_shouldNeverRevertgetTotalVotesAndState()
clamped_claimBribes(uint8)
property_shouldNeverRevertepoch()
governance_claimForInitiative(uint8)
property_GV_09()
excludeContracts()
governance_claimForInitiativeFuzzTest(uint8)
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)
property_viewTotalVotesAndStateEquivalency()
check_skip_consistecy(uint8)
governance_unregisterInitiative(uint8)
governance_claimFromStakingV1(uint8)
governance_allocateLQTY(int256[],int256[])
IS_TEST()
governance_depositLQTYViaPermit(uint256)
property_shouldNeverRevertgetInitiativeState_arbitrary(address)
property_sum_of_initatives_matches_total_votes_strict()
AssertionFailed(..)

Broken Properties

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

// forge test --match-test test_governance_withdrawLQTY_shouldRevertWhenClamped_ -vv 
 function test_governance_withdrawLQTY_shouldRevertWhenClamped_() public {

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_user_offset_is_always_greater_than_start_ -vv 
 function test_property_user_offset_is_always_greater_than_start_() public {

    vm.warp(block.timestamp + 462145);

    vm.roll(block.number + 1);

    offsetIsRational(1);

    vm.warp(block.timestamp + 14519);

    vm.roll(block.number + 1);

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 128153);
    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

// forge test --match-test test_property_sum_of_lqty_initiative_user_matches_ -vv 
 function test_property_sum_of_lqty_initiative_user_matches_() public {

    vm.warp(block.timestamp + 180341);

    vm.roll(block.number + 1);

    offsetIsRational(1);

    vm.warp(block.timestamp + 424467);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

// forge test --match-test test_withdrwaMustFailOnNonZeroAcc_ -vv 
 function test_withdrwaMustFailOnNonZeroAcc_() public {

    governance_depositLQTY(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

// forge test --match-test test_property_resetting_never_reverts_ -vv 
 function test_property_resetting_never_reverts_() public {

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

// forge test --match-test test_depositMustFailOnNonZeroAlloc_ -vv 
 function test_depositMustFailOnNonZeroAlloc_() public {

    offsetIsRational(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_global_offset_is_always_greater_than_start_ -vv 
 function test_property_global_offset_is_always_greater_than_start_() public {

    vm.warp(block.timestamp + 462144);

    vm.roll(block.number + 1);

    offsetIsRational(1);

    vm.warp(block.timestamp + 142712);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

Copy link

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

  • Fuzzer: ECHIDNA
  • Duration: 3h0s
  • Coverage: 43421
  • Failed: 8
  • Passed: 80

Results

Property Status
initiative_claimBribes(uint256,uint256,uint256,uint8)
check_unregisterable_consistecy(uint8)
check_claimable_solvency()
excludeSenders()
property_shouldNeverRevertgetInitiativeState(uint8)
check_realized_claiming_solvency()
targetInterfaces()
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)
helper_accrueBold(uint256)
property_BI02()
property_computingGlobalPowerNeverReverts()
governance_resetAllocations()
property_initiative_offset_matches_user_when_non_zero()
targetSenders()
targetContracts()
property_shouldGetTotalVotesAndState()
property_BI10()
property_shouldNeverRevertcalculateVotingThreshold()
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)
property_sum_of_user_voting_weights_strict()
property_sum_of_user_initiative_allocations()
property_summingInitiativesPowerNeverReverts()
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)
property_user_offset_is_always_greater_than_start()
helper_deployInitiative()
property_sum_of_lqty_global_user_matches()
property_sum_of_votes_in_bribes_match()
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)
targetArtifactSelectors()
property_sum_of_lqty_initiative_user_matches()
property_GV01()
property_viewCalculateVotingThreshold()
governance_registerInitiative(uint8)
initiative_depositBribe(uint256,uint256,uint256,uint8)
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)
property_BI07()
governance_resetAllocations_user_2()
targetArtifacts()
withdrwaMustFailOnNonZeroAcc(uint256)
property_sum_of_initatives_matches_total_votes_bounded()
property_BI04()
targetSelectors()
property_resetting_never_reverts(address[])
governance_depositLQTY_2(uint256)
governance_depositLQTY(uint256)
check_warmup_unregisterable_consistency(uint8)
property_ensure_user_alloc_cannot_dos()
property_BI08()
governance_withdrawLQTY(uint256)
property_sum_of_initatives_matches_total_votes_insolvency_assertion()
property_shouldNeverRevertgetLatestVotingThreshold()
governance_claimForInitiativeDoesntRevert(uint8)
property_BI03()
excludeSelectors()
excludeArtifacts()
check_claim_soundness()
property_shouldNeverRevertsecondsWithinEpoch()
failed()
property_sum_of_user_voting_weights_bounded()
property_BI01()
property_shouldNeverRevertepochStart(uint8)
property_BI09()
property_shouldNeverRevertSnapshotAndState(uint8)
property_shouldNeverRevertlqtyToVotes()
governance_snapshotVotesForInitiative(address)
governance_deployUserProxy()
depositMustFailOnNonZeroAlloc(uint256)
offsetIsRational(uint256)
property_allocations_are_never_dangerously_high()
property_global_offset_is_always_greater_than_start()
property_shouldNeverRevertgetTotalVotesAndState()
clamped_claimBribes(uint8)
property_shouldNeverRevertepoch()
governance_claimForInitiative(uint8)
property_GV_09()
excludeContracts()
governance_claimForInitiativeFuzzTest(uint8)
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)
property_viewTotalVotesAndStateEquivalency()
check_skip_consistecy(uint8)
governance_unregisterInitiative(uint8)
governance_claimFromStakingV1(uint8)
governance_allocateLQTY(int256[],int256[])
IS_TEST()
governance_depositLQTYViaPermit(uint256)
property_shouldNeverRevertgetInitiativeState_arbitrary(address)
property_sum_of_initatives_matches_total_votes_strict()
AssertionFailed(..)

Broken Properties

Broken property:

check_unregisterable_consistecy

Sequence

// forge test --match-test test_check_unregisterable_consistecy_ -vv 
 function test_check_unregisterable_consistecy_() public {

    vm.warp(block.timestamp + 282987);

    vm.roll(block.number + 1);

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 219527);
    governance_depositLQTY(1);

    vm.warp(block.timestamp + 686334);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    vm.warp(block.timestamp + 20769);

    vm.roll(block.number + 1);

    governance_resetAllocations();

    check_unregisterable_consistecy(0);

 }

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

// forge test --match-test test_governance_withdrawLQTY_shouldRevertWhenClamped_ -vv 
 function test_governance_withdrawLQTY_shouldRevertWhenClamped_() public {

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_user_offset_is_always_greater_than_start_ -vv 
 function test_property_user_offset_is_always_greater_than_start_() public {

    governance_depositLQTY_2(2);

    vm.warp(block.timestamp + 605434);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

// forge test --match-test test_property_sum_of_lqty_initiative_user_matches_ -vv 
 function test_property_sum_of_lqty_initiative_user_matches_() public {

    vm.warp(block.timestamp + 282788);

    vm.roll(block.number + 1);

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 322277);
    governance_depositLQTY(1);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

// forge test --match-test test_withdrwaMustFailOnNonZeroAcc_ -vv 
 function test_withdrwaMustFailOnNonZeroAcc_() public {

    governance_depositLQTY(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

// forge test --match-test test_property_resetting_never_reverts_ -vv 
 function test_property_resetting_never_reverts_() public {

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

// forge test --match-test test_depositMustFailOnNonZeroAlloc_ -vv 
 function test_depositMustFailOnNonZeroAlloc_() public {

    offsetIsRational(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_global_offset_is_always_greater_than_start_ -vv 
 function test_property_global_offset_is_always_greater_than_start_() public {

    governance_depositLQTY_2(2);

    vm.warp(block.timestamp + 490559);

    vm.roll(block.number + 1);

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 114260);
    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

Copy link

Recon Campaign Started

Copy link

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

  • Fuzzer: ECHIDNA
  • Duration: 3h11m32s
  • Coverage: 43416
  • Failed: 7
  • Passed: 81

Results

Property Status
initiative_claimBribes(uint256,uint256,uint256,uint8)
check_unregisterable_consistecy(uint8)
check_claimable_solvency()
excludeSenders()
property_shouldNeverRevertgetInitiativeState(uint8)
check_realized_claiming_solvency()
targetInterfaces()
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)
helper_accrueBold(uint256)
property_BI02()
property_computingGlobalPowerNeverReverts()
governance_resetAllocations()
property_initiative_offset_matches_user_when_non_zero()
targetSenders()
targetContracts()
property_shouldGetTotalVotesAndState()
property_BI10()
property_shouldNeverRevertcalculateVotingThreshold()
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)
property_sum_of_user_voting_weights_strict()
property_sum_of_user_initiative_allocations()
property_summingInitiativesPowerNeverReverts()
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)
property_user_offset_is_always_greater_than_start()
helper_deployInitiative()
property_sum_of_lqty_global_user_matches()
property_sum_of_votes_in_bribes_match()
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)
targetArtifactSelectors()
property_sum_of_lqty_initiative_user_matches()
property_GV01()
property_viewCalculateVotingThreshold()
governance_registerInitiative(uint8)
initiative_depositBribe(uint256,uint256,uint256,uint8)
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)
property_BI07()
governance_resetAllocations_user_2()
targetArtifacts()
withdrwaMustFailOnNonZeroAcc(uint256)
property_sum_of_initatives_matches_total_votes_bounded()
property_BI04()
targetSelectors()
property_resetting_never_reverts(address[])
governance_depositLQTY_2(uint256)
governance_depositLQTY(uint256)
check_warmup_unregisterable_consistency(uint8)
property_ensure_user_alloc_cannot_dos()
property_BI08()
governance_withdrawLQTY(uint256)
property_sum_of_initatives_matches_total_votes_insolvency_assertion()
property_shouldNeverRevertgetLatestVotingThreshold()
governance_claimForInitiativeDoesntRevert(uint8)
property_BI03()
excludeSelectors()
excludeArtifacts()
check_claim_soundness()
property_shouldNeverRevertsecondsWithinEpoch()
failed()
property_sum_of_user_voting_weights_bounded()
property_BI01()
property_shouldNeverRevertepochStart(uint8)
property_BI09()
property_shouldNeverRevertSnapshotAndState(uint8)
property_shouldNeverRevertlqtyToVotes()
governance_snapshotVotesForInitiative(address)
governance_deployUserProxy()
depositMustFailOnNonZeroAlloc(uint256)
offsetIsRational(uint256)
property_allocations_are_never_dangerously_high()
property_global_offset_is_always_greater_than_start()
property_shouldNeverRevertgetTotalVotesAndState()
clamped_claimBribes(uint8)
property_shouldNeverRevertepoch()
governance_claimForInitiative(uint8)
property_GV_09()
excludeContracts()
governance_claimForInitiativeFuzzTest(uint8)
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)
property_viewTotalVotesAndStateEquivalency()
check_skip_consistecy(uint8)
governance_unregisterInitiative(uint8)
governance_claimFromStakingV1(uint8)
governance_allocateLQTY(int256[],int256[])
IS_TEST()
governance_depositLQTYViaPermit(uint256)
property_shouldNeverRevertgetInitiativeState_arbitrary(address)
property_sum_of_initatives_matches_total_votes_strict()
AssertionFailed(..)

Broken Properties

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

// forge test --match-test test_governance_withdrawLQTY_shouldRevertWhenClamped_ -vv 
 function test_governance_withdrawLQTY_shouldRevertWhenClamped_() public {

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_user_offset_is_always_greater_than_start_ -vv 
 function test_property_user_offset_is_always_greater_than_start_() public {

    governance_depositLQTY_2(115792089237316195423570985008687907853269984665640564039457584007913129639923);

    vm.warp(block.timestamp + 605027);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,115792089237316195423570985008687907853269984665640564039457584007913129616046,0);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

// forge test --match-test test_property_sum_of_lqty_initiative_user_matches_ -vv 
 function test_property_sum_of_lqty_initiative_user_matches_() public {

    governance_depositLQTY_2(2);

    vm.warp(block.timestamp + 605056);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,0,1);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

// forge test --match-test test_withdrwaMustFailOnNonZeroAcc_ -vv 
 function test_withdrwaMustFailOnNonZeroAcc_() public {

    offsetIsRational(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

// forge test --match-test test_property_resetting_never_reverts_ -vv 
 function test_property_resetting_never_reverts_() public {

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

// forge test --match-test test_depositMustFailOnNonZeroAlloc_ -vv 
 function test_depositMustFailOnNonZeroAlloc_() public {

    governance_depositLQTY(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_global_offset_is_always_greater_than_start_ -vv 
 function test_property_global_offset_is_always_greater_than_start_() public {

    governance_depositLQTY_2(115792089237316195423570985008687907853269984665640564039457584007913129639923);

    vm.warp(block.timestamp + 605284);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,115792089237316195423570985008687907853269984665640564039457584007913129616046,0);

    property_global_offset_is_always_greater_than_start();

 }

Copy link

Recon Campaign Started

Copy link

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

  • Fuzzer: ECHIDNA
  • Duration: 5h48m24s
  • Coverage: 43567
  • Failed: 8
  • Passed: 80

Results

Property Status
initiative_claimBribes(uint256,uint256,uint256,uint8)
check_unregisterable_consistecy(uint8)
check_claimable_solvency()
excludeSenders()
property_shouldNeverRevertgetInitiativeState(uint8)
check_realized_claiming_solvency()
targetInterfaces()
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)
helper_accrueBold(uint256)
property_BI02()
property_computingGlobalPowerNeverReverts()
governance_resetAllocations()
property_initiative_offset_matches_user_when_non_zero()
targetSenders()
targetContracts()
property_shouldGetTotalVotesAndState()
property_BI10()
property_shouldNeverRevertcalculateVotingThreshold()
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)
property_sum_of_user_voting_weights_strict()
property_sum_of_user_initiative_allocations()
property_summingInitiativesPowerNeverReverts()
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)
property_user_offset_is_always_greater_than_start()
helper_deployInitiative()
property_sum_of_lqty_global_user_matches()
property_sum_of_votes_in_bribes_match()
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)
targetArtifactSelectors()
property_sum_of_lqty_initiative_user_matches()
property_GV01()
property_viewCalculateVotingThreshold()
governance_registerInitiative(uint8)
initiative_depositBribe(uint256,uint256,uint256,uint8)
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)
property_BI07()
governance_resetAllocations_user_2()
targetArtifacts()
withdrwaMustFailOnNonZeroAcc(uint256)
property_sum_of_initatives_matches_total_votes_bounded()
property_BI04()
targetSelectors()
property_resetting_never_reverts(address[])
governance_depositLQTY_2(uint256)
governance_depositLQTY(uint256)
check_warmup_unregisterable_consistency(uint8)
property_ensure_user_alloc_cannot_dos()
property_BI08()
governance_withdrawLQTY(uint256)
property_sum_of_initatives_matches_total_votes_insolvency_assertion()
property_shouldNeverRevertgetLatestVotingThreshold()
governance_claimForInitiativeDoesntRevert(uint8)
property_BI03()
excludeSelectors()
excludeArtifacts()
check_claim_soundness()
property_shouldNeverRevertsecondsWithinEpoch()
failed()
property_sum_of_user_voting_weights_bounded()
property_BI01()
property_shouldNeverRevertepochStart(uint8)
property_BI09()
property_shouldNeverRevertSnapshotAndState(uint8)
property_shouldNeverRevertlqtyToVotes()
governance_snapshotVotesForInitiative(address)
governance_deployUserProxy()
depositMustFailOnNonZeroAlloc(uint256)
offsetIsRational(uint256)
property_allocations_are_never_dangerously_high()
property_global_offset_is_always_greater_than_start()
property_shouldNeverRevertgetTotalVotesAndState()
clamped_claimBribes(uint8)
property_shouldNeverRevertepoch()
governance_claimForInitiative(uint8)
property_GV_09()
excludeContracts()
governance_claimForInitiativeFuzzTest(uint8)
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)
property_viewTotalVotesAndStateEquivalency()
check_skip_consistecy(uint8)
governance_unregisterInitiative(uint8)
governance_claimFromStakingV1(uint8)
governance_allocateLQTY(int256[],int256[])
IS_TEST()
governance_depositLQTYViaPermit(uint256)
property_shouldNeverRevertgetInitiativeState_arbitrary(address)
property_sum_of_initatives_matches_total_votes_strict()
AssertionFailed(..)

Broken Properties

Broken property:

check_unregisterable_consistecy

Sequence

// forge test --match-test test_check_unregisterable_consistecy_ -vv 
 function test_check_unregisterable_consistecy_() public {

    offsetIsRational(1);

    check_warmup_unregisterable_consistency(0);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    vm.warp(block.timestamp + 604836);

    vm.roll(block.number + 1);

    governance_resetAllocations();

    check_unregisterable_consistecy(0);

 }

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

// forge test --match-test test_governance_withdrawLQTY_shouldRevertWhenClamped_ -vv 
 function test_governance_withdrawLQTY_shouldRevertWhenClamped_() public {

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_user_offset_is_always_greater_than_start_ -vv 
 function test_property_user_offset_is_always_greater_than_start_() public {

    check_warmup_unregisterable_consistency(0);

    governance_depositLQTY_2(2);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,0,1);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

// forge test --match-test test_property_sum_of_lqty_initiative_user_matches_ -vv 
 function test_property_sum_of_lqty_initiative_user_matches_() public {

    check_warmup_unregisterable_consistency(0);

    governance_depositLQTY_2(2);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

// forge test --match-test test_withdrwaMustFailOnNonZeroAcc_ -vv 
 function test_withdrwaMustFailOnNonZeroAcc_() public {

    offsetIsRational(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

// forge test --match-test test_property_resetting_never_reverts_ -vv 
 function test_property_resetting_never_reverts_() public {

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

// forge test --match-test test_depositMustFailOnNonZeroAlloc_ -vv 
 function test_depositMustFailOnNonZeroAlloc_() public {

    offsetIsRational(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_global_offset_is_always_greater_than_start_ -vv 
 function test_property_global_offset_is_always_greater_than_start_() public {

     vm.roll(block.number + 1088);
     vm.warp(block.timestamp + 542442);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI10();

     vm.roll(block.number + 60289);
     vm.warp(block.timestamp + 20539);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTY_2(4370000);

    vm.warp(block.timestamp + 865761);

    vm.roll(block.number + 112243);

     vm.roll(block.number + 42264);
     vm.warp(block.timestamp + 322284);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI01();

     vm.roll(block.number + 44068);
     vm.warp(block.timestamp + 179668);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_allocateLQTY_clamped_single_initiative(46,59758112741496683744258210651293268891459357260859445081445093212486547368910,32892085976703057493429442155481922956792867770294738853359532131363189390811);

     vm.roll(block.number + 53429);
     vm.warp(block.timestamp + 226854);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI02();

     vm.roll(block.number + 14623);
     vm.warp(block.timestamp + 2);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_snapshotVotesForInitiative(0x0000000000000000000000000000000000030000);

     vm.roll(block.number + 58181);
     vm.warp(block.timestamp + 586021);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_computingGlobalPowerNeverReverts();

     vm.roll(block.number + 4901);
     vm.warp(block.timestamp + 336898);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_realized_claiming_solvency();

    vm.warp(block.timestamp + 478748);

    vm.roll(block.number + 51878);

     vm.roll(block.number + 44068);
     vm.warp(block.timestamp + 168836);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_summingInitiativesPowerNeverReverts();

     vm.roll(block.number + 25203);
     vm.warp(block.timestamp + 322176);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_viewCalculateVotingThreshold();

    vm.warp(block.timestamp + 784244);

    vm.roll(block.number + 78204);

     vm.roll(block.number + 11349);
     vm.warp(block.timestamp + 408775);
     vm.prank(0x0000000000000000000000000000000000010000);
    initiative_claimBribes(46940750882446099933503445504570747994449994777452419522159603995022003892459,115792089237316195423570985008687907853269984665640564019457584007913129639935,115792089237316195423570985008687907853269984665640564039457584007913129564896,68);

    vm.warp(block.timestamp + 405856);

    vm.roll(block.number + 40106);

     vm.roll(block.number + 33175);
     vm.warp(block.timestamp + 539433);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimForInitiativeFuzzTest(37);

     vm.roll(block.number + 24363);
     vm.warp(block.timestamp + 322343);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertcalculateVotingThreshold();

     vm.roll(block.number + 25398);
     vm.warp(block.timestamp + 403427);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_allocations_are_never_dangerously_high();

     vm.roll(block.number + 52344);
     vm.warp(block.timestamp + 322338);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_realized_claiming_solvency();

     vm.roll(block.number + 46153);
     vm.warp(block.timestamp + 518401);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_skip_consistecy(119);

    vm.warp(block.timestamp + 322377);

    vm.roll(block.number + 89);

     vm.roll(block.number + 20129);
     vm.warp(block.timestamp + 577177);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_initatives_matches_total_votes_insolvency_assertion();

     vm.roll(block.number + 30391);
     vm.warp(block.timestamp + 541203);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetInitiativeState_arbitrary(0x00000000000000000000000000000002fFffFffD);

     vm.roll(block.number + 24987);
     vm.warp(block.timestamp + 566553);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_summingInitiativesPowerNeverReverts();

     vm.roll(block.number + 4567);
     vm.warp(block.timestamp + 267436);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_allocations_are_never_dangerously_high();

     vm.roll(block.number + 8864);
     vm.warp(block.timestamp + 246073);
     vm.prank(0x0000000000000000000000000000000000020000);
    check_warmup_unregisterable_consistency(173);

     vm.roll(block.number + 25540);
     vm.warp(block.timestamp + 23767);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_initiative_offset_matches_user_when_non_zero();

     vm.roll(block.number + 4970);
     vm.warp(block.timestamp + 562841);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI08();

     vm.roll(block.number + 14625);
     vm.warp(block.timestamp + 91);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetInitiativeSnapshotAndState(157);

     vm.roll(block.number + 27112);
     vm.warp(block.timestamp + 155616);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_viewTotalVotesAndStateEquivalency();

     vm.roll(block.number + 40599);
     vm.warp(block.timestamp + 414007);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_viewCalculateVotingThreshold();

    vm.warp(block.timestamp + 67);

    vm.roll(block.number + 50947);

     vm.roll(block.number + 304);
     vm.warp(block.timestamp + 570946);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetTotalVotesAndState();

     vm.roll(block.number + 31461);
     vm.warp(block.timestamp + 304);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_initatives_matches_total_votes_bounded();

     vm.roll(block.number + 25538);
     vm.warp(block.timestamp + 177728);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_initatives_matches_total_votes_insolvency_assertion();

     vm.roll(block.number + 24224);
     vm.warp(block.timestamp + 341154);
     vm.prank(0x0000000000000000000000000000000000020000);
    clamped_claimBribes(156);

     vm.roll(block.number + 57086);
     vm.warp(block.timestamp + 80);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_voting_weights_strict();

    vm.warp(block.timestamp + 90605);

    vm.roll(block.number + 9999);

     vm.roll(block.number + 25158);
     vm.warp(block.timestamp + 490183);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_unregisterable_consistecy(43);

     vm.roll(block.number + 42);
     vm.warp(block.timestamp + 385974);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 12155);
     vm.warp(block.timestamp + 322254);
     vm.prank(0x0000000000000000000000000000000000030000);
    check_unregisterable_consistecy(33);

     vm.roll(block.number + 9966);
     vm.warp(block.timestamp + 222355);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_claimForInitiativeDoesntRevert(23);

     vm.roll(block.number + 59452);
     vm.warp(block.timestamp + 128965);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetInitiativeSnapshotAndState(31);

     vm.roll(block.number + 48651);
     vm.warp(block.timestamp + 463589);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_viewCalculateVotingThreshold();

     vm.roll(block.number + 29342);
     vm.warp(block.timestamp + 458443);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldGetTotalVotesAndState();

    vm.warp(block.timestamp + 230919);

    vm.roll(block.number + 5985);

     vm.roll(block.number + 55646);
     vm.warp(block.timestamp + 463587);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI07();

     vm.roll(block.number + 15368);
     vm.warp(block.timestamp + 150273);
     vm.prank(0x0000000000000000000000000000000000010000);
    clamped_claimBribes(31);

     vm.roll(block.number + 49923);
     vm.warp(block.timestamp + 79);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI02();

     vm.roll(block.number + 50537);
     vm.warp(block.timestamp + 230918);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI03();

     vm.roll(block.number + 4896);
     vm.warp(block.timestamp + 95);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI01();

     vm.roll(block.number + 53438);
     vm.warp(block.timestamp + 297344);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_viewCalculateVotingThreshold();

     vm.roll(block.number + 16926);
     vm.warp(block.timestamp + 320276);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimForInitiative(172);

    vm.warp(block.timestamp + 193409);

    vm.roll(block.number + 20123);

     vm.roll(block.number + 43283);
     vm.warp(block.timestamp + 468482);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_initiative_offset_matches_user_when_non_zero();

     vm.roll(block.number + 5021);
     vm.warp(block.timestamp + 326330);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_summingInitiativesPowerNeverReverts();

     vm.roll(block.number + 16616);
     vm.warp(block.timestamp + 21);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_allocations_are_never_dangerously_high();

     vm.roll(block.number + 31232);
     vm.warp(block.timestamp + 555653);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_global_offset_is_always_greater_than_start();

 }

Copy link

Recon Campaign Started

Copy link

Recon Campaign Started

Copy link

Recon Campaign Started

Copy link

Recon Campaign Started

Copy link

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

  • Fuzzer: ECHIDNA
  • Duration: 3h6m7s
  • Coverage: 44133
  • Failed: 7
  • Passed: 81

Results

Property Status
initiative_claimBribes(uint256,uint256,uint256,uint8)
check_unregisterable_consistecy(uint8)
check_claimable_solvency()
excludeSenders()
property_shouldNeverRevertgetInitiativeState(uint8)
check_realized_claiming_solvency()
targetInterfaces()
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)
helper_accrueBold(uint256)
property_BI02()
property_computingGlobalPowerNeverReverts()
governance_resetAllocations()
property_initiative_offset_matches_user_when_non_zero()
targetSenders()
targetContracts()
property_shouldGetTotalVotesAndState()
property_BI10()
property_shouldNeverRevertcalculateVotingThreshold()
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)
property_sum_of_user_voting_weights_strict()
property_sum_of_user_initiative_allocations()
property_summingInitiativesPowerNeverReverts()
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)
property_user_offset_is_always_greater_than_start()
helper_deployInitiative()
property_sum_of_lqty_global_user_matches()
property_sum_of_votes_in_bribes_match()
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)
targetArtifactSelectors()
property_sum_of_lqty_initiative_user_matches()
property_GV01()
property_viewCalculateVotingThreshold()
governance_registerInitiative(uint8)
initiative_depositBribe(uint256,uint256,uint256,uint8)
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)
property_BI07()
governance_resetAllocations_user_2()
targetArtifacts()
withdrwaMustFailOnNonZeroAcc(uint256)
property_sum_of_initatives_matches_total_votes_bounded()
property_BI04()
targetSelectors()
property_resetting_never_reverts(address[])
governance_depositLQTY_2(uint256)
governance_depositLQTY(uint256)
check_warmup_unregisterable_consistency(uint8)
property_ensure_user_alloc_cannot_dos()
property_BI08()
governance_withdrawLQTY(uint256)
property_sum_of_initatives_matches_total_votes_insolvency_assertion()
property_shouldNeverRevertgetLatestVotingThreshold()
governance_claimForInitiativeDoesntRevert(uint8)
property_BI03()
excludeSelectors()
excludeArtifacts()
check_claim_soundness()
property_shouldNeverRevertsecondsWithinEpoch()
failed()
property_sum_of_user_voting_weights_bounded()
property_BI01()
property_shouldNeverRevertepochStart(uint8)
property_BI09()
property_shouldNeverRevertSnapshotAndState(uint8)
property_shouldNeverRevertlqtyToVotes()
governance_snapshotVotesForInitiative(address)
governance_deployUserProxy()
depositMustFailOnNonZeroAlloc(uint256)
offsetIsRational(uint256)
property_allocations_are_never_dangerously_high()
property_global_offset_is_always_greater_than_start()
property_shouldNeverRevertgetTotalVotesAndState()
clamped_claimBribes(uint8)
property_shouldNeverRevertepoch()
governance_claimForInitiative(uint8)
property_GV_09()
excludeContracts()
governance_claimForInitiativeFuzzTest(uint8)
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)
property_viewTotalVotesAndStateEquivalency()
check_skip_consistecy(uint8)
governance_unregisterInitiative(uint8)
governance_claimFromStakingV1(uint8)
governance_allocateLQTY(int256[],int256[])
IS_TEST()
governance_depositLQTYViaPermit(uint256)
property_shouldNeverRevertgetInitiativeState_arbitrary(address)
property_sum_of_initatives_matches_total_votes_strict()
AssertionFailed(..)

Broken Properties

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

// forge test --match-test test_governance_withdrawLQTY_shouldRevertWhenClamped_ -vv 
 function test_governance_withdrawLQTY_shouldRevertWhenClamped_() public {

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_user_offset_is_always_greater_than_start_ -vv 
 function test_property_user_offset_is_always_greater_than_start_() public {

    vm.warp(block.timestamp + 604874);

    vm.roll(block.number + 1);

    offsetIsRational(1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

// forge test --match-test test_property_sum_of_lqty_initiative_user_matches_ -vv 
 function test_property_sum_of_lqty_initiative_user_matches_() public {

    vm.warp(block.timestamp + 65053);

    vm.roll(block.number + 1);

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 539766);
    offsetIsRational(1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

// forge test --match-test test_withdrwaMustFailOnNonZeroAcc_ -vv 
 function test_withdrwaMustFailOnNonZeroAcc_() public {

    offsetIsRational(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

// forge test --match-test test_property_resetting_never_reverts_ -vv 
 function test_property_resetting_never_reverts_() public {

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

// forge test --match-test test_depositMustFailOnNonZeroAlloc_ -vv 
 function test_depositMustFailOnNonZeroAlloc_() public {

    governance_depositLQTY(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_global_offset_is_always_greater_than_start_ -vv 
 function test_property_global_offset_is_always_greater_than_start_() public {

    offsetIsRational(1);

    vm.warp(block.timestamp + 604914);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

Copy link

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

  • Fuzzer: ECHIDNA
  • Duration: 3h8m31s
  • Coverage: 44134
  • Failed: 7
  • Passed: 81

Results

Property Status
initiative_claimBribes(uint256,uint256,uint256,uint8)
check_unregisterable_consistecy(uint8)
check_claimable_solvency()
excludeSenders()
property_shouldNeverRevertgetInitiativeState(uint8)
check_realized_claiming_solvency()
targetInterfaces()
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)
helper_accrueBold(uint256)
property_BI02()
property_computingGlobalPowerNeverReverts()
governance_resetAllocations()
property_initiative_offset_matches_user_when_non_zero()
targetSenders()
targetContracts()
property_shouldGetTotalVotesAndState()
property_BI10()
property_shouldNeverRevertcalculateVotingThreshold()
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)
property_sum_of_user_voting_weights_strict()
property_sum_of_user_initiative_allocations()
property_summingInitiativesPowerNeverReverts()
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)
property_user_offset_is_always_greater_than_start()
helper_deployInitiative()
property_sum_of_lqty_global_user_matches()
property_sum_of_votes_in_bribes_match()
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)
targetArtifactSelectors()
property_sum_of_lqty_initiative_user_matches()
property_GV01()
property_viewCalculateVotingThreshold()
governance_registerInitiative(uint8)
initiative_depositBribe(uint256,uint256,uint256,uint8)
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)
property_BI07()
governance_resetAllocations_user_2()
targetArtifacts()
withdrwaMustFailOnNonZeroAcc(uint256)
property_sum_of_initatives_matches_total_votes_bounded()
property_BI04()
targetSelectors()
property_resetting_never_reverts(address[])
governance_depositLQTY_2(uint256)
governance_depositLQTY(uint256)
check_warmup_unregisterable_consistency(uint8)
property_ensure_user_alloc_cannot_dos()
property_BI08()
governance_withdrawLQTY(uint256)
property_sum_of_initatives_matches_total_votes_insolvency_assertion()
property_shouldNeverRevertgetLatestVotingThreshold()
governance_claimForInitiativeDoesntRevert(uint8)
property_BI03()
excludeSelectors()
excludeArtifacts()
check_claim_soundness()
property_shouldNeverRevertsecondsWithinEpoch()
failed()
property_sum_of_user_voting_weights_bounded()
property_BI01()
property_shouldNeverRevertepochStart(uint8)
property_BI09()
property_shouldNeverRevertSnapshotAndState(uint8)
property_shouldNeverRevertlqtyToVotes()
governance_snapshotVotesForInitiative(address)
governance_deployUserProxy()
depositMustFailOnNonZeroAlloc(uint256)
offsetIsRational(uint256)
property_allocations_are_never_dangerously_high()
property_global_offset_is_always_greater_than_start()
property_shouldNeverRevertgetTotalVotesAndState()
clamped_claimBribes(uint8)
property_shouldNeverRevertepoch()
governance_claimForInitiative(uint8)
property_GV_09()
excludeContracts()
governance_claimForInitiativeFuzzTest(uint8)
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)
property_viewTotalVotesAndStateEquivalency()
check_skip_consistecy(uint8)
governance_unregisterInitiative(uint8)
governance_claimFromStakingV1(uint8)
governance_allocateLQTY(int256[],int256[])
IS_TEST()
governance_depositLQTYViaPermit(uint256)
property_shouldNeverRevertgetInitiativeState_arbitrary(address)
property_sum_of_initatives_matches_total_votes_strict()
AssertionFailed(..)

Broken Properties

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

// forge test --match-test test_governance_withdrawLQTY_shouldRevertWhenClamped_ -vv 
 function test_governance_withdrawLQTY_shouldRevertWhenClamped_() public {

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_user_offset_is_always_greater_than_start_ -vv 
 function test_property_user_offset_is_always_greater_than_start_() public {

    vm.warp(block.timestamp + 188165);

    vm.roll(block.number + 1);

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 416745);
    offsetIsRational(1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

// forge test --match-test test_property_sum_of_lqty_initiative_user_matches_ -vv 
 function test_property_sum_of_lqty_initiative_user_matches_() public {

    governance_depositLQTY(1);

    check_warmup_unregisterable_consistency(0);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

// forge test --match-test test_withdrwaMustFailOnNonZeroAcc_ -vv 
 function test_withdrwaMustFailOnNonZeroAcc_() public {

    governance_depositLQTY(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

// forge test --match-test test_property_resetting_never_reverts_ -vv 
 function test_property_resetting_never_reverts_() public {

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

// forge test --match-test test_depositMustFailOnNonZeroAlloc_ -vv 
 function test_depositMustFailOnNonZeroAlloc_() public {

    governance_depositLQTY(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_global_offset_is_always_greater_than_start_ -vv 
 function test_property_global_offset_is_always_greater_than_start_() public {

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 449571);
    offsetIsRational(1);

    vm.warp(block.timestamp + 155236);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

Copy link

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

  • Fuzzer: ECHIDNA
  • Duration: 3h8m34s
  • Coverage: 43631
  • Failed: 8
  • Passed: 80

Results

Property Status
initiative_claimBribes(uint256,uint256,uint256,uint8)
check_unregisterable_consistecy(uint8)
check_claimable_solvency()
excludeSenders()
property_shouldNeverRevertgetInitiativeState(uint8)
check_realized_claiming_solvency()
targetInterfaces()
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)
helper_accrueBold(uint256)
property_BI02()
property_computingGlobalPowerNeverReverts()
governance_resetAllocations()
property_initiative_offset_matches_user_when_non_zero()
targetSenders()
targetContracts()
property_shouldGetTotalVotesAndState()
property_BI10()
property_shouldNeverRevertcalculateVotingThreshold()
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)
property_sum_of_user_voting_weights_strict()
property_sum_of_user_initiative_allocations()
property_summingInitiativesPowerNeverReverts()
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)
property_user_offset_is_always_greater_than_start()
helper_deployInitiative()
property_sum_of_lqty_global_user_matches()
property_sum_of_votes_in_bribes_match()
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)
targetArtifactSelectors()
property_sum_of_lqty_initiative_user_matches()
property_GV01()
property_viewCalculateVotingThreshold()
governance_registerInitiative(uint8)
initiative_depositBribe(uint256,uint256,uint256,uint8)
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)
property_BI07()
governance_resetAllocations_user_2()
targetArtifacts()
withdrwaMustFailOnNonZeroAcc(uint256)
property_sum_of_initatives_matches_total_votes_bounded()
property_BI04()
targetSelectors()
property_resetting_never_reverts(address[])
governance_depositLQTY_2(uint256)
governance_depositLQTY(uint256)
check_warmup_unregisterable_consistency(uint8)
property_ensure_user_alloc_cannot_dos()
property_BI08()
governance_withdrawLQTY(uint256)
property_sum_of_initatives_matches_total_votes_insolvency_assertion()
property_shouldNeverRevertgetLatestVotingThreshold()
governance_claimForInitiativeDoesntRevert(uint8)
property_BI03()
excludeSelectors()
excludeArtifacts()
check_claim_soundness()
property_shouldNeverRevertsecondsWithinEpoch()
failed()
property_sum_of_user_voting_weights_bounded()
property_BI01()
property_shouldNeverRevertepochStart(uint8)
property_BI09()
property_shouldNeverRevertSnapshotAndState(uint8)
property_shouldNeverRevertlqtyToVotes()
governance_snapshotVotesForInitiative(address)
governance_deployUserProxy()
depositMustFailOnNonZeroAlloc(uint256)
offsetIsRational(uint256)
property_allocations_are_never_dangerously_high()
property_global_offset_is_always_greater_than_start()
property_shouldNeverRevertgetTotalVotesAndState()
clamped_claimBribes(uint8)
property_shouldNeverRevertepoch()
governance_claimForInitiative(uint8)
property_GV_09()
excludeContracts()
governance_claimForInitiativeFuzzTest(uint8)
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)
property_viewTotalVotesAndStateEquivalency()
check_skip_consistecy(uint8)
governance_unregisterInitiative(uint8)
governance_claimFromStakingV1(uint8)
governance_allocateLQTY(int256[],int256[])
IS_TEST()
governance_depositLQTYViaPermit(uint256)
property_shouldNeverRevertgetInitiativeState_arbitrary(address)
property_sum_of_initatives_matches_total_votes_strict()
AssertionFailed(..)

Broken Properties

Broken property:

check_unregisterable_consistecy

Sequence

// forge test --match-test test_check_unregisterable_consistecy_ -vv 
 function test_check_unregisterable_consistecy_() public {

    vm.warp(block.timestamp + 132218);

    vm.roll(block.number + 1);

    offsetIsRational(1);

    check_warmup_unregisterable_consistency(0);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    vm.warp(block.timestamp + 472630);

    vm.roll(block.number + 1);

    governance_resetAllocations();

    check_unregisterable_consistecy(0);

 }

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

// forge test --match-test test_governance_withdrawLQTY_shouldRevertWhenClamped_ -vv 
 function test_governance_withdrawLQTY_shouldRevertWhenClamped_() public {

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_user_offset_is_always_greater_than_start_ -vv 
 function test_property_user_offset_is_always_greater_than_start_() public {

    governance_depositLQTY_2(2);

    vm.warp(block.timestamp + 605233);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

// forge test --match-test test_property_sum_of_lqty_initiative_user_matches_ -vv 
 function test_property_sum_of_lqty_initiative_user_matches_() public {

    vm.warp(block.timestamp + 336734);

    vm.roll(block.number + 1);

    governance_depositLQTY(1);

    vm.warp(block.timestamp + 268094);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

// forge test --match-test test_withdrwaMustFailOnNonZeroAcc_ -vv 
 function test_withdrwaMustFailOnNonZeroAcc_() public {

    offsetIsRational(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

// forge test --match-test test_property_resetting_never_reverts_ -vv 
 function test_property_resetting_never_reverts_() public {

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

// forge test --match-test test_depositMustFailOnNonZeroAlloc_ -vv 
 function test_depositMustFailOnNonZeroAlloc_() public {

    governance_depositLQTY(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_global_offset_is_always_greater_than_start_ -vv 
 function test_property_global_offset_is_always_greater_than_start_() public {

    vm.warp(block.timestamp + 32408);

    vm.roll(block.number + 1);

    governance_depositLQTY_2(2);

    vm.warp(block.timestamp + 572414);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

Copy link

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

  • Fuzzer: ECHIDNA
  • Duration: 12h21m52s
  • Coverage: 43534
  • Failed: 7
  • Passed: 81

Results

Property Status
initiative_claimBribes(uint256,uint256,uint256,uint8)
check_unregisterable_consistecy(uint8)
check_claimable_solvency()
excludeSenders()
property_shouldNeverRevertgetInitiativeState(uint8)
check_realized_claiming_solvency()
targetInterfaces()
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)
helper_accrueBold(uint256)
property_BI02()
property_computingGlobalPowerNeverReverts()
governance_resetAllocations()
property_initiative_offset_matches_user_when_non_zero()
targetSenders()
targetContracts()
property_shouldGetTotalVotesAndState()
property_BI10()
property_shouldNeverRevertcalculateVotingThreshold()
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)
property_sum_of_user_voting_weights_strict()
property_sum_of_user_initiative_allocations()
property_summingInitiativesPowerNeverReverts()
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)
property_user_offset_is_always_greater_than_start()
helper_deployInitiative()
property_sum_of_lqty_global_user_matches()
property_sum_of_votes_in_bribes_match()
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)
targetArtifactSelectors()
property_sum_of_lqty_initiative_user_matches()
property_GV01()
property_viewCalculateVotingThreshold()
governance_registerInitiative(uint8)
initiative_depositBribe(uint256,uint256,uint256,uint8)
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)
property_BI07()
governance_resetAllocations_user_2()
targetArtifacts()
withdrwaMustFailOnNonZeroAcc(uint256)
property_sum_of_initatives_matches_total_votes_bounded()
property_BI04()
targetSelectors()
property_resetting_never_reverts(address[])
governance_depositLQTY_2(uint256)
governance_depositLQTY(uint256)
check_warmup_unregisterable_consistency(uint8)
property_ensure_user_alloc_cannot_dos()
property_BI08()
governance_withdrawLQTY(uint256)
property_sum_of_initatives_matches_total_votes_insolvency_assertion()
property_shouldNeverRevertgetLatestVotingThreshold()
governance_claimForInitiativeDoesntRevert(uint8)
property_BI03()
excludeSelectors()
excludeArtifacts()
check_claim_soundness()
property_shouldNeverRevertsecondsWithinEpoch()
failed()
property_sum_of_user_voting_weights_bounded()
property_BI01()
property_shouldNeverRevertepochStart(uint8)
property_BI09()
property_shouldNeverRevertSnapshotAndState(uint8)
property_shouldNeverRevertlqtyToVotes()
governance_snapshotVotesForInitiative(address)
governance_deployUserProxy()
depositMustFailOnNonZeroAlloc(uint256)
offsetIsRational(uint256)
property_allocations_are_never_dangerously_high()
property_global_offset_is_always_greater_than_start()
property_shouldNeverRevertgetTotalVotesAndState()
clamped_claimBribes(uint8)
property_shouldNeverRevertepoch()
governance_claimForInitiative(uint8)
property_GV_09()
excludeContracts()
governance_claimForInitiativeFuzzTest(uint8)
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)
property_viewTotalVotesAndStateEquivalency()
check_skip_consistecy(uint8)
governance_unregisterInitiative(uint8)
governance_claimFromStakingV1(uint8)
governance_allocateLQTY(int256[],int256[])
IS_TEST()
governance_depositLQTYViaPermit(uint256)
property_shouldNeverRevertgetInitiativeState_arbitrary(address)
property_sum_of_initatives_matches_total_votes_strict()
AssertionFailed(..)

Broken Properties

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

// forge test --match-test test_governance_withdrawLQTY_shouldRevertWhenClamped_ -vv 
 function test_governance_withdrawLQTY_shouldRevertWhenClamped_() public {

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_user_offset_is_always_greater_than_start_ -vv 
 function test_property_user_offset_is_always_greater_than_start_() public {

    check_warmup_unregisterable_consistency(0);

    offsetIsRational(1);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

// forge test --match-test test_property_sum_of_lqty_initiative_user_matches_ -vv 
 function test_property_sum_of_lqty_initiative_user_matches_() public {

     vm.roll(block.number + 5065);
     vm.warp(block.timestamp + 176489);
     vm.prank(0x0000000000000000000000000000000000030000);
    check_claimable_solvency();

     vm.roll(block.number + 5792);
     vm.warp(block.timestamp + 42);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_lqty_initiative_user_matches();

     vm.roll(block.number + 31680);
     vm.warp(block.timestamp + 157408);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_summingInitiativesPowerNeverReverts();

     vm.roll(block.number + 44802);
     vm.warp(block.timestamp + 157408);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimForInitiativeFuzzTest(251);

     vm.roll(block.number + 37747);
     vm.warp(block.timestamp + 322377);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_summingInitiativesPowerNeverReverts();

     vm.roll(block.number + 39162);
     vm.warp(block.timestamp + 383589);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertepoch();

     vm.roll(block.number + 13535);
     vm.warp(block.timestamp + 364336);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_depositLQTY_2(30271982452169318454359169969229696728725359473106328336480899763061634663126);

     vm.roll(block.number + 40542);
     vm.warp(block.timestamp + 75039);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_viewCalculateVotingThreshold();

     vm.roll(block.number + 21599);
     vm.warp(block.timestamp + 322291);
     vm.prank(0x0000000000000000000000000000000000030000);
    check_claimable_solvency();

    vm.warp(block.timestamp + 878303);

    vm.roll(block.number + 55865);

     vm.roll(block.number + 200);
     vm.warp(block.timestamp + 322365);
     vm.prank(0x0000000000000000000000000000000000030000);
    IS_TEST();

     vm.roll(block.number + 20129);
     vm.warp(block.timestamp + 171500);
     vm.prank(0x0000000000000000000000000000000000030000);
    clamped_claimBribes(223);

     vm.roll(block.number + 257);
     vm.warp(block.timestamp + 6);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_skip_consistecy(1);

     vm.roll(block.number + 44394);
     vm.warp(block.timestamp + 492633);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_warmup_unregisterable_consistency(244);

     vm.roll(block.number + 39209);
     vm.warp(block.timestamp + 322142);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_allocateLQTY_clamped_single_initiative(120,54318004069326067303995936419509914555080158202328288664976155362672750182326,36661408324494480576580360917921683576629554177966215595708964783359695787409);

     vm.roll(block.number + 5792);
     vm.warp(block.timestamp + 86349);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 34823);
     vm.warp(block.timestamp + 322307);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_allocations_are_never_dangerously_high();

    vm.warp(block.timestamp + 898677);

    vm.roll(block.number + 67);

     vm.roll(block.number + 49415);
     vm.warp(block.timestamp + 306);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetInitiativeSnapshotAndState(66);

     vm.roll(block.number + 54721);
     vm.warp(block.timestamp + 321627);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI07();

     vm.prank(0x0000000000000000000000000000000000020000);
    check_claim_soundness();

    vm.warp(block.timestamp + 293990);

    vm.roll(block.number + 67);

     vm.roll(block.number + 2497);
     vm.warp(block.timestamp + 569382);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetInitiativeSnapshotAndState(37);

     vm.roll(block.number + 45261);
     vm.warp(block.timestamp + 78);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_lqty_global_user_matches();

     vm.roll(block.number + 18213);
     vm.warp(block.timestamp + 267435);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI03();

    vm.warp(block.timestamp + 494138);

    vm.roll(block.number + 44879);

     vm.roll(block.number + 50327);
     vm.warp(block.timestamp + 63697);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI02();

     vm.roll(block.number + 31313);
     vm.warp(block.timestamp + 144646);
     vm.prank(0x0000000000000000000000000000000000020000);
    helper_deployInitiative();

     vm.roll(block.number + 23721);
     vm.warp(block.timestamp + 449696);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_claim_soundness();

     vm.roll(block.number + 54809);
     vm.warp(block.timestamp + 178399);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetInitiativeState_arbitrary(0x0000000000000000000000000000000000010000);

     vm.roll(block.number + 30505);
     vm.warp(block.timestamp + 458441);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_votes_in_bribes_match();

     vm.roll(block.number + 456);
     vm.warp(block.timestamp + 207834);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_user_offset_is_always_greater_than_start();

     vm.roll(block.number + 23721);
     vm.warp(block.timestamp + 236464);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_lqty_initiative_user_matches();

     vm.roll(block.number + 21601);
     vm.warp(block.timestamp + 89);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_snapshotVotesForInitiative(0x00000000000000000000000000000001fffffffE);

     vm.roll(block.number + 5017);
     vm.warp(block.timestamp + 555652);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_GV01();

    vm.warp(block.timestamp + 173595);

    vm.roll(block.number + 50536);

     vm.roll(block.number + 57919);
     vm.warp(block.timestamp + 568143);
     vm.prank(0x0000000000000000000000000000000000020000);
    helper_deployInitiative();

     vm.roll(block.number + 56920);
     vm.warp(block.timestamp + 247336);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI04();

    vm.warp(block.timestamp + 1170030);

    vm.roll(block.number + 20554);

     vm.roll(block.number + 32959);
     vm.warp(block.timestamp + 202688);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI10();

     vm.roll(block.number + 1001);
     vm.warp(block.timestamp + 590278);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_user_offset_is_always_greater_than_start();

    vm.warp(block.timestamp + 541305);

    vm.roll(block.number + 5);

     vm.roll(block.number + 6944);
     vm.warp(block.timestamp + 221593);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_initatives_matches_total_votes_strict();

     vm.roll(block.number + 35001);
     vm.warp(block.timestamp + 562425);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertsecondsWithinEpoch();

    vm.warp(block.timestamp + 153418);

    vm.roll(block.number + 2819);

     vm.roll(block.number + 48651);
     vm.warp(block.timestamp + 179668);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimForInitiativeDoesntRevert(154);

    vm.warp(block.timestamp + 574795);

    vm.roll(block.number + 36279);

     vm.roll(block.number + 54329);
     vm.warp(block.timestamp + 344203);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI08();

     vm.roll(block.number + 46305);
     vm.warp(block.timestamp + 95);
     vm.prank(0x0000000000000000000000000000000000030000);
    helper_accrueBold(115792089237316195423570985008687907853269984665640564039457584007913129639735);

     vm.roll(block.number + 50882);
     vm.warp(block.timestamp + 490181);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_registerInitiative(221);

     vm.roll(block.number + 12338);
     vm.warp(block.timestamp + 246073);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimForInitiativeDoesntRevert(28);

    vm.warp(block.timestamp + 144647);

    vm.roll(block.number + 5023);

     vm.roll(block.number + 30505);
     vm.warp(block.timestamp + 547623);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_voting_weights_strict();

     vm.roll(block.number + 3906);
     vm.warp(block.timestamp + 249334);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_viewCalculateVotingThreshold();

    vm.warp(block.timestamp + 648706);

    vm.roll(block.number + 52039);

     vm.roll(block.number + 13626);
     vm.warp(block.timestamp + 254);
     vm.prank(0x0000000000000000000000000000000000010000);
    clamped_claimBribes(92);

     vm.roll(block.number + 25504);
     vm.warp(block.timestamp + 385873);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_GV_09();

     vm.roll(block.number + 13050);
     vm.warp(block.timestamp + 209930);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI01();

     vm.roll(block.number + 13707);
     vm.warp(block.timestamp + 590279);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_user_voting_weights_strict();

     vm.roll(block.number + 3601);
     vm.warp(block.timestamp + 2099);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTY(1000000000000000000000);

    vm.warp(block.timestamp + 374306);

    vm.roll(block.number + 33825);

     vm.roll(block.number + 33823);
     vm.warp(block.timestamp + 445681);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_depositLQTY(24191999);

     vm.roll(block.number + 68);
     vm.warp(block.timestamp + 179666);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI10();

     vm.roll(block.number + 31461);
     vm.warp(block.timestamp + 168836);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_viewCalculateVotingThreshold();

     vm.roll(block.number + 17667);
     vm.warp(block.timestamp + 73040);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_initiative_allocations();

     vm.roll(block.number + 15090);
     vm.warp(block.timestamp + 45911);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertsnapshotVotesForInitiative(216);

     vm.roll(block.number + 49925);
     vm.warp(block.timestamp + 149580);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_global_offset_is_always_greater_than_start();

     vm.roll(block.number + 122);
     vm.warp(block.timestamp + 54939);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_viewCalculateVotingThreshold();

     vm.roll(block.number + 33825);
     vm.warp(block.timestamp + 322262);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_viewTotalVotesAndStateEquivalency();

     vm.roll(block.number + 37070);
     vm.warp(block.timestamp + 26295);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTY_2(47728079488397370013867886287047876098169179848615796776542618999907481089859);

     vm.roll(block.number + 30784);
     vm.warp(block.timestamp + 155524);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_claimForInitiativeFuzzTest(0);

     vm.roll(block.number + 14467);
     vm.warp(block.timestamp + 221592);
     vm.prank(0x0000000000000000000000000000000000020000);
    check_skip_consistecy(111);

     vm.roll(block.number + 33200);
     vm.warp(block.timestamp + 322333);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_initiative_offset_matches_user_when_non_zero();

     vm.roll(block.number + 232);
     vm.warp(block.timestamp + 337669);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI09();

     vm.roll(block.number + 4702);
     vm.warp(block.timestamp + 191304);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetTotalVotesAndState();

    vm.warp(block.timestamp + 21600);

    vm.roll(block.number + 19811);

     vm.roll(block.number + 26842);
     vm.warp(block.timestamp + 555653);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 51799);
     vm.warp(block.timestamp + 474988);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_initatives_matches_total_votes_bounded();

     vm.roll(block.number + 5215);
     vm.warp(block.timestamp + 322311);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertcalculateVotingThreshold();

     vm.roll(block.number + 2512);
     vm.warp(block.timestamp + 41430);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI07();

    vm.warp(block.timestamp + 730714);

    vm.roll(block.number + 9163);

     vm.roll(block.number + 35678);
     vm.warp(block.timestamp + 262803);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_viewCalculateVotingThreshold();

     vm.roll(block.number + 304);
     vm.warp(block.timestamp + 82671);
     vm.prank(0x0000000000000000000000000000000000020000);
    offsetIsRational(621);

     vm.roll(block.number + 12493);
     vm.warp(block.timestamp + 32767);
     vm.prank(0x0000000000000000000000000000000000030000);
    offsetIsRational(51410465162090333642258627402894042234883010866795703786681236120536859592458);

    vm.warp(block.timestamp + 321376);

    vm.roll(block.number + 35680);

     vm.roll(block.number + 4957);
     vm.warp(block.timestamp + 351629);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_snapshotVotesForInitiative(0x537C8f3d3E18dF5517a58B3fB9D9143697996802);

     vm.roll(block.number + 23722);
     vm.warp(block.timestamp + 562840);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_computingGlobalPowerNeverReverts();

     vm.roll(block.number + 13706);
     vm.warp(block.timestamp + 276994);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

// forge test --match-test test_withdrwaMustFailOnNonZeroAcc_ -vv 
 function test_withdrwaMustFailOnNonZeroAcc_() public {

    offsetIsRational(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

// forge test --match-test test_property_resetting_never_reverts_ -vv 
 function test_property_resetting_never_reverts_() public {

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

// forge test --match-test test_depositMustFailOnNonZeroAlloc_ -vv 
 function test_depositMustFailOnNonZeroAlloc_() public {

    offsetIsRational(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

// forge test --match-test test_property_global_offset_is_always_greater_than_start_ -vv 
 function test_property_global_offset_is_always_greater_than_start_() public {

    vm.warp(block.timestamp + 460796);

    vm.roll(block.number + 1);

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 144080);
    governance_depositLQTY(1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants